T:Type.
T    (x:T, L:T List. sorted(L)  no_repeats(T;L)  no_repeats(T;s-insert(x;L))) 

latex

Definitions

t  T, sorted(L), no_repeats(T;l), P  Q, x:A. B(x), ||as||, {i..j}, l[i], AB, , Prop, A, s-insert(x;l), (x  l), False, P & Q, P  Q, P  Q, True, ij, b, b, , i<j, T, Unit, i=j, P  Q, xL. P(x)

Lemmas

member-s-insert, l member wf, cons member, sorted-cons, no repeats wf, sorted wf, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, bool wf, bnot wf, assert wf, le int wf, no repeats cons, s-insert wf, nat wf, not wf, int seg wf, le wf, select wf, length wf2